/* Benchmarks for the PionterC verifier. */

// pointer dereference


/*@ {p}N && i>999 */
int f(int* p, int i)
{
  *p = 9;
  *p = 9;
  *p = 9;
  *p = 9;
  return i;
}
/*@  result>99 */